YES 2.05
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((lookup :: Eq a => [a] -> [([a],b)] -> Maybe b) :: Eq a => [a] -> [([a],b)] -> Maybe b) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((lookup :: Eq a => [a] -> [([a],b)] -> Maybe b) :: Eq a => [a] -> [([a],b)] -> Maybe b) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
lookup | k [] | = Nothing |
lookup | k ((x,y) : xys) | |
is transformed to
lookup | k [] | = lookup3 k [] |
lookup | k ((x,y) : xys) | = lookup2 k ((x,y) : xys) |
lookup0 | k x y xys True | = lookup k xys |
lookup1 | k x y xys True | = Just y |
lookup1 | k x y xys False | = lookup0 k x y xys otherwise |
lookup2 | k ((x,y) : xys) | = lookup1 k x y xys (k == x) |
lookup3 | k [] | = Nothing |
lookup3 | xy xz | = lookup2 xy xz |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (lookup :: Eq b => [b] -> [([b],a)] -> Maybe a) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(yu3400), Succ(yu40001000)) → new_primPlusNat(yu3400, yu40001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(yu3400), Succ(yu40001000)) → new_primPlusNat(yu3400, yu40001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(yu30100), Succ(yu4000100)) → new_primMulNat(yu30100, Succ(yu4000100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(yu30100), Succ(yu4000100)) → new_primMulNat(yu30100, Succ(yu4000100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(yu3000), Succ(yu400000)) → new_primEqNat(yu3000, yu400000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(yu3000), Succ(yu400000)) → new_primEqNat(yu3000, yu400000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs0(Right(yu300), Right(yu40000), de, app(app(ty_@2, eb), ec)) → new_esEs2(yu300, yu40000, eb, ec)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(yu302, yu40002, bdb, bdc, bdd)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(app(ty_@2, he), hf)) → new_esEs2(yu301, yu40001, he, hf)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(ty_Maybe, ha)) → new_esEs(yu301, yu40001, ha)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_Maybe, fh), fb) → new_esEs(yu300, yu40000, fh)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_Maybe, bab), fd, ff) → new_esEs(yu300, yu40000, bab)
new_esEs(Just(yu300), Just(yu40000), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(yu300, yu40000, bg, bh, ca)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(ty_[], bcg)) → new_esEs1(yu302, yu40002, bcg)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), fg) → new_esEs1(yu311, yu40011, fg)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_@2, gd), ge), fb) → new_esEs2(yu300, yu40000, gd, ge)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(ty_[], eh)) → new_esEs1(yu310, yu40010, eh)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(app(app(ty_@3, hg), hh), baa)) → new_esEs3(yu301, yu40001, hg, hh, baa)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(ty_[], bbf), ff) → new_esEs1(yu301, yu40001, bbf)
new_esEs0(Left(yu300), Left(yu40000), app(app(app(ty_@3, db), dc), dd), cc) → new_esEs3(yu300, yu40000, db, dc, dd)
new_esEs(Just(yu300), Just(yu40000), app(ty_Maybe, ba)) → new_esEs(yu300, yu40000, ba)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(app(ty_Either, hb), hc)) → new_esEs0(yu301, yu40001, hb, hc)
new_esEs0(Left(yu300), Left(yu40000), app(app(ty_Either, cd), ce), cc) → new_esEs0(yu300, yu40000, cd, ce)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(ty_Maybe, bbc), ff) → new_esEs(yu301, yu40001, bbc)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_[], gc), fb) → new_esEs1(yu300, yu40000, gc)
new_esEs0(Left(yu300), Left(yu40000), app(app(ty_@2, cg), da), cc) → new_esEs2(yu300, yu40000, cg, da)
new_esEs0(Right(yu300), Right(yu40000), de, app(app(app(ty_@3, ed), ee), ef)) → new_esEs3(yu300, yu40000, ed, ee, ef)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(ty_Maybe, bcd)) → new_esEs(yu302, yu40002, bcd)
new_esEs0(Right(yu300), Right(yu40000), de, app(app(ty_Either, dg), dh)) → new_esEs0(yu300, yu40000, dg, dh)
new_esEs(Just(yu300), Just(yu40000), app(app(ty_Either, bb), bc)) → new_esEs0(yu300, yu40000, bb, bc)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(app(app(ty_@3, bca), bcb), bcc), ff) → new_esEs3(yu301, yu40001, bca, bcb, bcc)
new_esEs(Just(yu300), Just(yu40000), app(app(ty_@2, be), bf)) → new_esEs2(yu300, yu40000, be, bf)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(ty_Either, de), cc)) → new_esEs0(yu310, yu40010, de, cc)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(app(ty_@2, bch), bda)) → new_esEs2(yu302, yu40002, bch, bda)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_@2, baf), bag), fd, ff) → new_esEs2(yu300, yu40000, baf, bag)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(app(ty_@2, bbg), bbh), ff) → new_esEs2(yu301, yu40001, bbg, bbh)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(ty_Maybe, eg)) → new_esEs(yu310, yu40010, eg)
new_esEs0(Right(yu300), Right(yu40000), de, app(ty_[], ea)) → new_esEs1(yu300, yu40000, ea)
new_esEs(Just(yu300), Just(yu40000), app(ty_[], bd)) → new_esEs1(yu300, yu40000, bd)
new_esEs0(Left(yu300), Left(yu40000), app(ty_[], cf), cc) → new_esEs1(yu300, yu40000, cf)
new_esEs0(Right(yu300), Right(yu40000), de, app(ty_Maybe, df)) → new_esEs(yu300, yu40000, df)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(app(ty_@3, fc), fd), ff)) → new_esEs3(yu310, yu40010, fc, fd, ff)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(ty_@2, fa), fb)) → new_esEs2(yu310, yu40010, fa, fb)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_[], bae), fd, ff) → new_esEs1(yu300, yu40000, bae)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_Either, ga), gb), fb) → new_esEs0(yu300, yu40000, ga, gb)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(ty_[], hd)) → new_esEs1(yu301, yu40001, hd)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(app(ty_Either, bbd), bbe), ff) → new_esEs0(yu301, yu40001, bbd, bbe)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(app(ty_Either, bce), bcf)) → new_esEs0(yu302, yu40002, bce, bcf)
new_esEs0(Left(yu300), Left(yu40000), app(ty_Maybe, cb), cc) → new_esEs(yu300, yu40000, cb)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(app(ty_@3, bah), bba), bbb), fd, ff) → new_esEs3(yu300, yu40000, bah, bba, bbb)
new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(app(app(ty_@3, gf), gg), gh), fb) → new_esEs3(yu300, yu40000, gf, gg, gh)
new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_Either, bac), bad), fd, ff) → new_esEs0(yu300, yu40000, bac, bad)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs(Just(yu300), Just(yu40000), app(app(ty_Either, bb), bc)) → new_esEs0(yu300, yu40000, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(yu300), Just(yu40000), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(yu300, yu40000, bg, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Just(yu300), Just(yu40000), app(app(ty_@2, be), bf)) → new_esEs2(yu300, yu40000, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(ty_Either, de), cc)) → new_esEs0(yu310, yu40010, de, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(app(ty_@3, fc), fd), ff)) → new_esEs3(yu310, yu40010, fc, fd, ff)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(ty_@2, fa), fb)) → new_esEs2(yu310, yu40010, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(yu300), Just(yu40000), app(ty_Maybe, ba)) → new_esEs(yu300, yu40000, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(yu300), Just(yu40000), app(ty_[], bd)) → new_esEs1(yu300, yu40000, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(ty_Maybe, eg)) → new_esEs(yu310, yu40010, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(app(ty_Either, hb), hc)) → new_esEs0(yu301, yu40001, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_Either, ga), gb), fb) → new_esEs0(yu300, yu40000, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(app(app(ty_@3, hg), hh), baa)) → new_esEs3(yu301, yu40001, hg, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(app(app(ty_@3, gf), gg), gh), fb) → new_esEs3(yu300, yu40000, gf, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(app(ty_@2, he), hf)) → new_esEs2(yu301, yu40001, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(app(ty_@2, gd), ge), fb) → new_esEs2(yu300, yu40000, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(ty_Maybe, ha)) → new_esEs(yu301, yu40001, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_Maybe, fh), fb) → new_esEs(yu300, yu40000, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), app(ty_[], gc), fb) → new_esEs1(yu300, yu40000, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(@2(yu300, yu301), @2(yu40000, yu40001), fa, app(ty_[], hd)) → new_esEs1(yu301, yu40001, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(app(ty_Either, bbd), bbe), ff) → new_esEs0(yu301, yu40001, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(app(ty_Either, bce), bcf)) → new_esEs0(yu302, yu40002, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_Either, bac), bad), fd, ff) → new_esEs0(yu300, yu40000, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Left(yu300), Left(yu40000), app(app(ty_Either, cd), ce), cc) → new_esEs0(yu300, yu40000, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Right(yu300), Right(yu40000), de, app(app(ty_Either, dg), dh)) → new_esEs0(yu300, yu40000, dg, dh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(yu302, yu40002, bdb, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(app(app(ty_@3, bca), bcb), bcc), ff) → new_esEs3(yu301, yu40001, bca, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(app(ty_@3, bah), bba), bbb), fd, ff) → new_esEs3(yu300, yu40000, bah, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(app(ty_@2, bch), bda)) → new_esEs2(yu302, yu40002, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(app(ty_@2, bbg), bbh), ff) → new_esEs2(yu301, yu40001, bbg, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(app(ty_@2, baf), bag), fd, ff) → new_esEs2(yu300, yu40000, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_Maybe, bab), fd, ff) → new_esEs(yu300, yu40000, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(ty_Maybe, bbc), ff) → new_esEs(yu301, yu40001, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(ty_Maybe, bcd)) → new_esEs(yu302, yu40002, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, fd, app(ty_[], bcg)) → new_esEs1(yu302, yu40002, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), fc, app(ty_[], bbf), ff) → new_esEs1(yu301, yu40001, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), app(ty_[], bae), fd, ff) → new_esEs1(yu300, yu40000, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Left(yu300), Left(yu40000), app(app(app(ty_@3, db), dc), dd), cc) → new_esEs3(yu300, yu40000, db, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Right(yu300), Right(yu40000), de, app(app(app(ty_@3, ed), ee), ef)) → new_esEs3(yu300, yu40000, ed, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(Right(yu300), Right(yu40000), de, app(app(ty_@2, eb), ec)) → new_esEs2(yu300, yu40000, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(Left(yu300), Left(yu40000), app(app(ty_@2, cg), da), cc) → new_esEs2(yu300, yu40000, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(yu310, yu311), :(yu40010, yu40011), fg) → new_esEs1(yu311, yu40011, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(ty_[], eh)) → new_esEs1(yu310, yu40010, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(yu300), Right(yu40000), de, app(ty_Maybe, df)) → new_esEs(yu300, yu40000, df)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(Left(yu300), Left(yu40000), app(ty_Maybe, cb), cc) → new_esEs(yu300, yu40000, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(yu300), Right(yu40000), de, app(ty_[], ea)) → new_esEs1(yu300, yu40000, ea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(Left(yu300), Left(yu40000), app(ty_[], cf), cc) → new_esEs1(yu300, yu40000, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_lookup(:(yu30, yu31), :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup1(yu30, yu31, yu4000, yu4001, yu401, yu41, new_asAs(new_esEs4(yu30, yu4000, bd), new_esEs5(yu31, yu4001, bd)), bc, bd)
new_lookup(:(yu30, yu31), :(@2([], yu401), yu41), bc, bd) → new_lookup(:(yu30, yu31), yu41, bc, bd)
new_lookup1(yu13, yu14, yu15, yu16, yu17, yu18, False, ba, bb) → new_lookup(:(yu13, yu14), yu18, ba, bb)
new_lookup([], :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup([], yu41, bc, bd)
The TRS R consists of the following rules:
new_esEs9(Left(yu300), Left(yu40000), ty_@0, bg) → new_esEs7(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu3400, yu40001000)))
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_esEs21(yu302, yu40002, ty_Integer) → new_esEs15(yu302, yu40002)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu30, yu4000, cc, cd, ce)
new_esEs5([], [], bd) → True
new_esEs21(yu302, yu40002, ty_Ordering) → new_esEs11(yu302, yu40002)
new_esEs20(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Bool, bg) → new_esEs10(yu300, yu40000)
new_esEs11(EQ, EQ) → True
new_esEs23(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs14(yu300, yu40000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, app(ty_Ratio, hh)) → new_esEs18(yu300, yu40000, hh)
new_esEs18(:%(yu300, yu301), :%(yu40000, yu40001), cf) → new_asAs(new_esEs25(yu300, yu40000, cf), new_esEs26(yu301, yu40001, cf))
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs21(yu302, yu40002, app(ty_[], bbf)) → new_esEs5(yu302, yu40002, bbf)
new_esEs20(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_[], ee)) → new_esEs5(yu300, yu40000, ee)
new_esEs4(yu30, yu4000, app(ty_Ratio, cf)) → new_esEs18(yu30, yu4000, cf)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_Either, ec), ed)) → new_esEs9(yu300, yu40000, ec, ed)
new_esEs5([], :(yu40010, yu40011), bd) → False
new_esEs5(:(yu310, yu311), [], bd) → False
new_esEs4(yu30, yu4000, app(ty_Maybe, be)) → new_esEs6(yu30, yu4000, be)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Maybe, cg), bg) → new_esEs6(yu300, yu40000, cg)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs7(yu300, yu40000)
new_esEs11(GT, LT) → False
new_esEs11(LT, GT) → False
new_esEs20(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_@2, bda), bdb)) → new_esEs12(yu300, yu40000, bda, bdb)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs25(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Char, bg) → new_esEs14(yu300, yu40000)
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs9(Left(yu300), Left(yu40000), ty_Ordering, bg) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs11(EQ, LT) → False
new_esEs11(LT, EQ) → False
new_esEs8(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs22(yu310, yu40010, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), cc, cd, ce) → new_asAs(new_esEs19(yu300, yu40000, cc), new_asAs(new_esEs20(yu301, yu40001, cd), new_esEs21(yu302, yu40002, ce)))
new_esEs22(yu310, yu40010, app(ty_Maybe, be)) → new_esEs6(yu310, yu40010, be)
new_esEs15(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs11(yu30, yu4000)
new_esEs20(yu301, yu40001, app(app(ty_@2, bae), baf)) → new_esEs12(yu301, yu40001, bae, baf)
new_esEs4(yu30, yu4000, ty_Float) → new_esEs17(yu30, yu4000)
new_esEs10(True, True) → True
new_esEs20(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs22(yu310, yu40010, app(ty_Ratio, cf)) → new_esEs18(yu310, yu40010, cf)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs22(yu310, yu40010, ty_Float) → new_esEs17(yu310, yu40010)
new_esEs4(yu30, yu4000, app(ty_[], bh)) → new_esEs5(yu30, yu4000, bh)
new_esEs20(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_Either, bcf), bcg)) → new_esEs9(yu300, yu40000, bcf, bcg)
new_esEs22(yu310, yu40010, app(app(ty_Either, bf), bg)) → new_esEs9(yu310, yu40010, bf, bg)
new_esEs20(yu301, yu40001, app(ty_[], bad)) → new_esEs5(yu301, yu40001, bad)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(yu300, yu40000, app(ty_Ratio, bdf)) → new_esEs18(yu300, yu40000, bdf)
new_esEs19(yu300, yu40000, app(app(ty_@2, hc), hd)) → new_esEs12(yu300, yu40000, hc, hd)
new_esEs20(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs26(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs19(yu300, yu40000, app(ty_Maybe, gg)) → new_esEs6(yu300, yu40000, gg)
new_esEs23(yu300, yu40000, app(ty_[], bch)) → new_esEs5(yu300, yu40000, bch)
new_esEs21(yu302, yu40002, app(app(app(ty_@3, bca), bcb), bcc)) → new_esEs13(yu302, yu40002, bca, bcb, bcc)
new_esEs25(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_@2, ef), eg)) → new_esEs12(yu300, yu40000, ef, eg)
new_esEs21(yu302, yu40002, app(app(ty_@2, bbg), bbh)) → new_esEs12(yu302, yu40002, bbg, bbh)
new_esEs20(yu301, yu40001, app(ty_Ratio, bbb)) → new_esEs18(yu301, yu40001, bbb)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, gc), gd), ge)) → new_esEs13(yu300, yu40000, gc, gd, ge)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], fh)) → new_esEs5(yu300, yu40000, fh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(app(ty_@3, eh), fa), fb)) → new_esEs13(yu300, yu40000, eh, fa, fb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, app(ty_[], bh)) → new_esEs5(yu310, yu40010, bh)
new_esEs20(yu301, yu40001, app(app(ty_Either, bab), bac)) → new_esEs9(yu301, yu40001, bab, bac)
new_esEs9(Left(yu300), Left(yu40000), app(ty_[], dc), bg) → new_esEs5(yu300, yu40000, dc)
new_esEs19(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(ty_@2, bec), bed)) → new_esEs12(yu301, yu40001, bec, bed)
new_esEs11(GT, GT) → True
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs20(yu301, yu40001, app(ty_Maybe, baa)) → new_esEs6(yu301, yu40001, baa)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs15(yu300, yu40000)
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_asAs(False, yu33) → False
new_esEs19(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_primEqNat0(Zero, Zero) → True
new_esEs19(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Maybe, eb)) → new_esEs6(yu300, yu40000, eb)
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs19(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, fd)) → new_esEs6(yu300, yu40000, fd)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs10(yu30, yu4000)
new_esEs21(yu302, yu40002, ty_Int) → new_esEs16(yu302, yu40002)
new_esEs19(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs13(yu300, yu40000, bdc, bdd, bde)
new_esEs22(yu310, yu40010, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu310, yu40010, cc, cd, ce)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_Either, da), db), bg) → new_esEs9(yu300, yu40000, da, db)
new_esEs23(yu300, yu40000, app(ty_Maybe, bce)) → new_esEs6(yu300, yu40000, bce)
new_esEs19(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs21(yu302, yu40002, ty_@0) → new_esEs7(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_[], beb)) → new_esEs5(yu301, yu40001, beb)
new_esEs22(yu310, yu40010, ty_@0) → new_esEs7(yu310, yu40010)
new_primPlusNat0(Succ(yu340), yu4000100) → Succ(Succ(new_primPlusNat1(yu340, yu4000100)))
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs20(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, ff), fg)) → new_esEs9(yu300, yu40000, ff, fg)
new_esEs19(yu300, yu40000, app(app(app(ty_@3, he), hf), hg)) → new_esEs13(yu300, yu40000, he, hf, hg)
new_esEs14(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs19(yu300, yu40000, app(app(ty_Either, gh), ha)) → new_esEs9(yu300, yu40000, gh, ha)
new_esEs22(yu310, yu40010, ty_Char) → new_esEs14(yu310, yu40010)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs20(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs8(yu30, yu4000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Left(yu300), Left(yu40000), ty_Float, bg) → new_esEs17(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Zero) → Succ(yu3400)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs16(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Double, bg) → new_esEs8(yu300, yu40000)
new_esEs4(yu30, yu4000, app(app(ty_@2, ca), cb)) → new_esEs12(yu30, yu4000, ca, cb)
new_esEs4(yu30, yu4000, app(app(ty_Either, bf), bg)) → new_esEs9(yu30, yu4000, bf, bg)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs15(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Integer, bg) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(app(ty_@3, bee), bef), beg)) → new_esEs13(yu301, yu40001, bee, bef, beg)
new_esEs21(yu302, yu40002, ty_Double) → new_esEs8(yu302, yu40002)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Integer) → new_esEs15(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_esEs9(Left(yu300), Left(yu40000), ty_Int, bg) → new_esEs16(yu300, yu40000)
new_esEs20(yu301, yu40001, app(app(app(ty_@3, bag), bah), bba)) → new_esEs13(yu301, yu40001, bag, bah, bba)
new_esEs17(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs19(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, ty_Integer) → new_esEs15(yu310, yu40010)
new_esEs10(False, False) → True
new_esEs21(yu302, yu40002, ty_Float) → new_esEs17(yu302, yu40002)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs22(yu310, yu40010, app(app(ty_@2, ca), cb)) → new_esEs12(yu310, yu40010, ca, cb)
new_asAs(True, yu33) → yu33
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs8(yu300, yu40000)
new_esEs11(LT, LT) → True
new_esEs4(yu30, yu4000, ty_@0) → new_esEs7(yu30, yu4000)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs24(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs22(yu310, yu40010, ty_Double) → new_esEs8(yu310, yu40010)
new_esEs6(Nothing, Nothing, be) → True
new_esEs21(yu302, yu40002, ty_Char) → new_esEs14(yu302, yu40002)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs9(Left(yu300), Left(yu40000), app(app(app(ty_@3, df), dg), dh), bg) → new_esEs13(yu300, yu40000, df, dg, dh)
new_esEs21(yu302, yu40002, app(ty_Maybe, bbc)) → new_esEs6(yu302, yu40002, bbc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, ga), gb)) → new_esEs12(yu300, yu40000, ga, gb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs24(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs6(Nothing, Just(yu40000), be) → False
new_esEs6(Just(yu300), Nothing, be) → False
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs11(GT, EQ) → False
new_esEs11(EQ, GT) → False
new_esEs24(yu301, yu40001, app(ty_Maybe, bdg)) → new_esEs6(yu301, yu40001, bdg)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Ratio, ea), bg) → new_esEs18(yu300, yu40000, ea)
new_esEs21(yu302, yu40002, ty_Bool) → new_esEs10(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_Ratio, beh)) → new_esEs18(yu301, yu40001, beh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Ratio, fc)) → new_esEs18(yu300, yu40000, fc)
new_esEs7(@0, @0) → True
new_esEs21(yu302, yu40002, app(app(ty_Either, bbd), bbe)) → new_esEs9(yu302, yu40002, bbd, bbe)
new_esEs12(@2(yu300, yu301), @2(yu40000, yu40001), ca, cb) → new_asAs(new_esEs23(yu300, yu40000, ca), new_esEs24(yu301, yu40001, cb))
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_@2, dd), de), bg) → new_esEs12(yu300, yu40000, dd, de)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs14(yu30, yu4000)
new_esEs19(yu300, yu40000, app(ty_[], hb)) → new_esEs5(yu300, yu40000, hb)
new_esEs24(yu301, yu40001, app(app(ty_Either, bdh), bea)) → new_esEs9(yu301, yu40001, bdh, bea)
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_esEs22(yu310, yu40010, ty_Ordering) → new_esEs11(yu310, yu40010)
new_esEs9(Right(yu300), Left(yu40000), bf, bg) → False
new_esEs9(Left(yu300), Right(yu40000), bf, bg) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs21(yu302, yu40002, app(ty_Ratio, bcd)) → new_esEs18(yu302, yu40002, bcd)
new_esEs22(yu310, yu40010, ty_Int) → new_esEs16(yu310, yu40010)
new_esEs5(:(yu310, yu311), :(yu40010, yu40011), bd) → new_asAs(new_esEs22(yu310, yu40010, bd), new_esEs5(yu311, yu40011, bd))
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, gf)) → new_esEs18(yu300, yu40000, gf)
The set Q consists of the following terms:
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_lookup([], :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup([], yu41, bc, bd)
The TRS R consists of the following rules:
new_esEs9(Left(yu300), Left(yu40000), ty_@0, bg) → new_esEs7(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu3400, yu40001000)))
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_esEs21(yu302, yu40002, ty_Integer) → new_esEs15(yu302, yu40002)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu30, yu4000, cc, cd, ce)
new_esEs5([], [], bd) → True
new_esEs21(yu302, yu40002, ty_Ordering) → new_esEs11(yu302, yu40002)
new_esEs20(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Bool, bg) → new_esEs10(yu300, yu40000)
new_esEs11(EQ, EQ) → True
new_esEs23(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs14(yu300, yu40000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, app(ty_Ratio, hh)) → new_esEs18(yu300, yu40000, hh)
new_esEs18(:%(yu300, yu301), :%(yu40000, yu40001), cf) → new_asAs(new_esEs25(yu300, yu40000, cf), new_esEs26(yu301, yu40001, cf))
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs21(yu302, yu40002, app(ty_[], bbf)) → new_esEs5(yu302, yu40002, bbf)
new_esEs20(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_[], ee)) → new_esEs5(yu300, yu40000, ee)
new_esEs4(yu30, yu4000, app(ty_Ratio, cf)) → new_esEs18(yu30, yu4000, cf)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_Either, ec), ed)) → new_esEs9(yu300, yu40000, ec, ed)
new_esEs5([], :(yu40010, yu40011), bd) → False
new_esEs5(:(yu310, yu311), [], bd) → False
new_esEs4(yu30, yu4000, app(ty_Maybe, be)) → new_esEs6(yu30, yu4000, be)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Maybe, cg), bg) → new_esEs6(yu300, yu40000, cg)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs7(yu300, yu40000)
new_esEs11(GT, LT) → False
new_esEs11(LT, GT) → False
new_esEs20(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_@2, bda), bdb)) → new_esEs12(yu300, yu40000, bda, bdb)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs25(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Char, bg) → new_esEs14(yu300, yu40000)
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs9(Left(yu300), Left(yu40000), ty_Ordering, bg) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs11(EQ, LT) → False
new_esEs11(LT, EQ) → False
new_esEs8(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs22(yu310, yu40010, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), cc, cd, ce) → new_asAs(new_esEs19(yu300, yu40000, cc), new_asAs(new_esEs20(yu301, yu40001, cd), new_esEs21(yu302, yu40002, ce)))
new_esEs22(yu310, yu40010, app(ty_Maybe, be)) → new_esEs6(yu310, yu40010, be)
new_esEs15(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs11(yu30, yu4000)
new_esEs20(yu301, yu40001, app(app(ty_@2, bae), baf)) → new_esEs12(yu301, yu40001, bae, baf)
new_esEs4(yu30, yu4000, ty_Float) → new_esEs17(yu30, yu4000)
new_esEs10(True, True) → True
new_esEs20(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs22(yu310, yu40010, app(ty_Ratio, cf)) → new_esEs18(yu310, yu40010, cf)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs22(yu310, yu40010, ty_Float) → new_esEs17(yu310, yu40010)
new_esEs4(yu30, yu4000, app(ty_[], bh)) → new_esEs5(yu30, yu4000, bh)
new_esEs20(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_Either, bcf), bcg)) → new_esEs9(yu300, yu40000, bcf, bcg)
new_esEs22(yu310, yu40010, app(app(ty_Either, bf), bg)) → new_esEs9(yu310, yu40010, bf, bg)
new_esEs20(yu301, yu40001, app(ty_[], bad)) → new_esEs5(yu301, yu40001, bad)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(yu300, yu40000, app(ty_Ratio, bdf)) → new_esEs18(yu300, yu40000, bdf)
new_esEs19(yu300, yu40000, app(app(ty_@2, hc), hd)) → new_esEs12(yu300, yu40000, hc, hd)
new_esEs20(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs26(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs19(yu300, yu40000, app(ty_Maybe, gg)) → new_esEs6(yu300, yu40000, gg)
new_esEs23(yu300, yu40000, app(ty_[], bch)) → new_esEs5(yu300, yu40000, bch)
new_esEs21(yu302, yu40002, app(app(app(ty_@3, bca), bcb), bcc)) → new_esEs13(yu302, yu40002, bca, bcb, bcc)
new_esEs25(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_@2, ef), eg)) → new_esEs12(yu300, yu40000, ef, eg)
new_esEs21(yu302, yu40002, app(app(ty_@2, bbg), bbh)) → new_esEs12(yu302, yu40002, bbg, bbh)
new_esEs20(yu301, yu40001, app(ty_Ratio, bbb)) → new_esEs18(yu301, yu40001, bbb)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, gc), gd), ge)) → new_esEs13(yu300, yu40000, gc, gd, ge)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], fh)) → new_esEs5(yu300, yu40000, fh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(app(ty_@3, eh), fa), fb)) → new_esEs13(yu300, yu40000, eh, fa, fb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, app(ty_[], bh)) → new_esEs5(yu310, yu40010, bh)
new_esEs20(yu301, yu40001, app(app(ty_Either, bab), bac)) → new_esEs9(yu301, yu40001, bab, bac)
new_esEs9(Left(yu300), Left(yu40000), app(ty_[], dc), bg) → new_esEs5(yu300, yu40000, dc)
new_esEs19(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(ty_@2, bec), bed)) → new_esEs12(yu301, yu40001, bec, bed)
new_esEs11(GT, GT) → True
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs20(yu301, yu40001, app(ty_Maybe, baa)) → new_esEs6(yu301, yu40001, baa)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs15(yu300, yu40000)
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_asAs(False, yu33) → False
new_esEs19(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_primEqNat0(Zero, Zero) → True
new_esEs19(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Maybe, eb)) → new_esEs6(yu300, yu40000, eb)
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs19(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, fd)) → new_esEs6(yu300, yu40000, fd)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs10(yu30, yu4000)
new_esEs21(yu302, yu40002, ty_Int) → new_esEs16(yu302, yu40002)
new_esEs19(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs13(yu300, yu40000, bdc, bdd, bde)
new_esEs22(yu310, yu40010, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu310, yu40010, cc, cd, ce)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_Either, da), db), bg) → new_esEs9(yu300, yu40000, da, db)
new_esEs23(yu300, yu40000, app(ty_Maybe, bce)) → new_esEs6(yu300, yu40000, bce)
new_esEs19(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs21(yu302, yu40002, ty_@0) → new_esEs7(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_[], beb)) → new_esEs5(yu301, yu40001, beb)
new_esEs22(yu310, yu40010, ty_@0) → new_esEs7(yu310, yu40010)
new_primPlusNat0(Succ(yu340), yu4000100) → Succ(Succ(new_primPlusNat1(yu340, yu4000100)))
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs20(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, ff), fg)) → new_esEs9(yu300, yu40000, ff, fg)
new_esEs19(yu300, yu40000, app(app(app(ty_@3, he), hf), hg)) → new_esEs13(yu300, yu40000, he, hf, hg)
new_esEs14(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs19(yu300, yu40000, app(app(ty_Either, gh), ha)) → new_esEs9(yu300, yu40000, gh, ha)
new_esEs22(yu310, yu40010, ty_Char) → new_esEs14(yu310, yu40010)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs20(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs8(yu30, yu4000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Left(yu300), Left(yu40000), ty_Float, bg) → new_esEs17(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Zero) → Succ(yu3400)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs16(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Double, bg) → new_esEs8(yu300, yu40000)
new_esEs4(yu30, yu4000, app(app(ty_@2, ca), cb)) → new_esEs12(yu30, yu4000, ca, cb)
new_esEs4(yu30, yu4000, app(app(ty_Either, bf), bg)) → new_esEs9(yu30, yu4000, bf, bg)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs15(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Integer, bg) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(app(ty_@3, bee), bef), beg)) → new_esEs13(yu301, yu40001, bee, bef, beg)
new_esEs21(yu302, yu40002, ty_Double) → new_esEs8(yu302, yu40002)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Integer) → new_esEs15(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_esEs9(Left(yu300), Left(yu40000), ty_Int, bg) → new_esEs16(yu300, yu40000)
new_esEs20(yu301, yu40001, app(app(app(ty_@3, bag), bah), bba)) → new_esEs13(yu301, yu40001, bag, bah, bba)
new_esEs17(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs19(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, ty_Integer) → new_esEs15(yu310, yu40010)
new_esEs10(False, False) → True
new_esEs21(yu302, yu40002, ty_Float) → new_esEs17(yu302, yu40002)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs22(yu310, yu40010, app(app(ty_@2, ca), cb)) → new_esEs12(yu310, yu40010, ca, cb)
new_asAs(True, yu33) → yu33
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs8(yu300, yu40000)
new_esEs11(LT, LT) → True
new_esEs4(yu30, yu4000, ty_@0) → new_esEs7(yu30, yu4000)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs24(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs22(yu310, yu40010, ty_Double) → new_esEs8(yu310, yu40010)
new_esEs6(Nothing, Nothing, be) → True
new_esEs21(yu302, yu40002, ty_Char) → new_esEs14(yu302, yu40002)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs9(Left(yu300), Left(yu40000), app(app(app(ty_@3, df), dg), dh), bg) → new_esEs13(yu300, yu40000, df, dg, dh)
new_esEs21(yu302, yu40002, app(ty_Maybe, bbc)) → new_esEs6(yu302, yu40002, bbc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, ga), gb)) → new_esEs12(yu300, yu40000, ga, gb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs24(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs6(Nothing, Just(yu40000), be) → False
new_esEs6(Just(yu300), Nothing, be) → False
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs11(GT, EQ) → False
new_esEs11(EQ, GT) → False
new_esEs24(yu301, yu40001, app(ty_Maybe, bdg)) → new_esEs6(yu301, yu40001, bdg)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Ratio, ea), bg) → new_esEs18(yu300, yu40000, ea)
new_esEs21(yu302, yu40002, ty_Bool) → new_esEs10(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_Ratio, beh)) → new_esEs18(yu301, yu40001, beh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Ratio, fc)) → new_esEs18(yu300, yu40000, fc)
new_esEs7(@0, @0) → True
new_esEs21(yu302, yu40002, app(app(ty_Either, bbd), bbe)) → new_esEs9(yu302, yu40002, bbd, bbe)
new_esEs12(@2(yu300, yu301), @2(yu40000, yu40001), ca, cb) → new_asAs(new_esEs23(yu300, yu40000, ca), new_esEs24(yu301, yu40001, cb))
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_@2, dd), de), bg) → new_esEs12(yu300, yu40000, dd, de)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs14(yu30, yu4000)
new_esEs19(yu300, yu40000, app(ty_[], hb)) → new_esEs5(yu300, yu40000, hb)
new_esEs24(yu301, yu40001, app(app(ty_Either, bdh), bea)) → new_esEs9(yu301, yu40001, bdh, bea)
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_esEs22(yu310, yu40010, ty_Ordering) → new_esEs11(yu310, yu40010)
new_esEs9(Right(yu300), Left(yu40000), bf, bg) → False
new_esEs9(Left(yu300), Right(yu40000), bf, bg) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs21(yu302, yu40002, app(ty_Ratio, bcd)) → new_esEs18(yu302, yu40002, bcd)
new_esEs22(yu310, yu40010, ty_Int) → new_esEs16(yu310, yu40010)
new_esEs5(:(yu310, yu311), :(yu40010, yu40011), bd) → new_asAs(new_esEs22(yu310, yu40010, bd), new_esEs5(yu311, yu40011, bd))
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, gf)) → new_esEs18(yu300, yu40000, gf)
The set Q consists of the following terms:
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_lookup([], :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup([], yu41, bc, bd)
R is empty.
The set Q consists of the following terms:
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_lookup([], :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup([], yu41, bc, bd)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_lookup([], :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup([], yu41, bc, bd)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_lookup(:(yu30, yu31), :(@2([], yu401), yu41), bc, bd) → new_lookup(:(yu30, yu31), yu41, bc, bd)
new_lookup(:(yu30, yu31), :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup1(yu30, yu31, yu4000, yu4001, yu401, yu41, new_asAs(new_esEs4(yu30, yu4000, bd), new_esEs5(yu31, yu4001, bd)), bc, bd)
new_lookup1(yu13, yu14, yu15, yu16, yu17, yu18, False, ba, bb) → new_lookup(:(yu13, yu14), yu18, ba, bb)
The TRS R consists of the following rules:
new_esEs9(Left(yu300), Left(yu40000), ty_@0, bg) → new_esEs7(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Succ(yu40001000)) → Succ(Succ(new_primPlusNat1(yu3400, yu40001000)))
new_primEqInt(Pos(Succ(yu3000)), Neg(yu40000)) → False
new_primEqInt(Neg(Succ(yu3000)), Pos(yu40000)) → False
new_esEs23(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_primEqInt(Pos(Zero), Neg(Succ(yu400000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(yu400000))) → False
new_esEs21(yu302, yu40002, ty_Integer) → new_esEs15(yu302, yu40002)
new_esEs4(yu30, yu4000, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu30, yu4000, cc, cd, ce)
new_esEs5([], [], bd) → True
new_esEs21(yu302, yu40002, ty_Ordering) → new_esEs11(yu302, yu40002)
new_esEs20(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Bool, bg) → new_esEs10(yu300, yu40000)
new_esEs11(EQ, EQ) → True
new_esEs23(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Char) → new_esEs14(yu300, yu40000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, app(ty_Ratio, hh)) → new_esEs18(yu300, yu40000, hh)
new_esEs18(:%(yu300, yu301), :%(yu40000, yu40001), cf) → new_asAs(new_esEs25(yu300, yu40000, cf), new_esEs26(yu301, yu40001, cf))
new_esEs6(Just(yu300), Just(yu40000), ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs21(yu302, yu40002, app(ty_[], bbf)) → new_esEs5(yu302, yu40002, bbf)
new_esEs20(yu301, yu40001, ty_Ordering) → new_esEs11(yu301, yu40001)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_[], ee)) → new_esEs5(yu300, yu40000, ee)
new_esEs4(yu30, yu4000, app(ty_Ratio, cf)) → new_esEs18(yu30, yu4000, cf)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_Either, ec), ed)) → new_esEs9(yu300, yu40000, ec, ed)
new_esEs5([], :(yu40010, yu40011), bd) → False
new_esEs5(:(yu310, yu311), [], bd) → False
new_esEs4(yu30, yu4000, app(ty_Maybe, be)) → new_esEs6(yu30, yu4000, be)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Maybe, cg), bg) → new_esEs6(yu300, yu40000, cg)
new_primPlusNat0(Zero, yu4000100) → Succ(yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_@0) → new_esEs7(yu300, yu40000)
new_esEs11(GT, LT) → False
new_esEs11(LT, GT) → False
new_esEs20(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_@2, bda), bdb)) → new_esEs12(yu300, yu40000, bda, bdb)
new_esEs6(Just(yu300), Just(yu40000), ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs25(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs9(Left(yu300), Left(yu40000), ty_Char, bg) → new_esEs14(yu300, yu40000)
new_sr(Neg(yu3010), Pos(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_sr(Pos(yu3010), Neg(yu400010)) → Neg(new_primMulNat0(yu3010, yu400010))
new_esEs9(Left(yu300), Left(yu40000), ty_Ordering, bg) → new_esEs11(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs11(EQ, LT) → False
new_esEs11(LT, EQ) → False
new_esEs8(Double(yu300, yu301), Double(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs22(yu310, yu40010, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs13(@3(yu300, yu301, yu302), @3(yu40000, yu40001, yu40002), cc, cd, ce) → new_asAs(new_esEs19(yu300, yu40000, cc), new_asAs(new_esEs20(yu301, yu40001, cd), new_esEs21(yu302, yu40002, ce)))
new_esEs22(yu310, yu40010, app(ty_Maybe, be)) → new_esEs6(yu310, yu40010, be)
new_esEs15(Integer(yu300), Integer(yu40000)) → new_primEqInt(yu300, yu40000)
new_esEs4(yu30, yu4000, ty_Ordering) → new_esEs11(yu30, yu4000)
new_esEs20(yu301, yu40001, app(app(ty_@2, bae), baf)) → new_esEs12(yu301, yu40001, bae, baf)
new_esEs4(yu30, yu4000, ty_Float) → new_esEs17(yu30, yu4000)
new_esEs10(True, True) → True
new_esEs20(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs22(yu310, yu40010, app(ty_Ratio, cf)) → new_esEs18(yu310, yu40010, cf)
new_primEqNat0(Zero, Succ(yu400000)) → False
new_primEqNat0(Succ(yu3000), Zero) → False
new_esEs22(yu310, yu40010, ty_Float) → new_esEs17(yu310, yu40010)
new_esEs4(yu30, yu4000, app(ty_[], bh)) → new_esEs5(yu30, yu4000, bh)
new_esEs20(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs23(yu300, yu40000, app(app(ty_Either, bcf), bcg)) → new_esEs9(yu300, yu40000, bcf, bcg)
new_esEs22(yu310, yu40010, app(app(ty_Either, bf), bg)) → new_esEs9(yu310, yu40010, bf, bg)
new_esEs20(yu301, yu40001, app(ty_[], bad)) → new_esEs5(yu301, yu40001, bad)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs23(yu300, yu40000, app(ty_Ratio, bdf)) → new_esEs18(yu300, yu40000, bdf)
new_esEs19(yu300, yu40000, app(app(ty_@2, hc), hd)) → new_esEs12(yu300, yu40000, hc, hd)
new_esEs20(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs26(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs19(yu300, yu40000, app(ty_Maybe, gg)) → new_esEs6(yu300, yu40000, gg)
new_esEs23(yu300, yu40000, app(ty_[], bch)) → new_esEs5(yu300, yu40000, bch)
new_esEs21(yu302, yu40002, app(app(app(ty_@3, bca), bcb), bcc)) → new_esEs13(yu302, yu40002, bca, bcb, bcc)
new_esEs25(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(ty_@2, ef), eg)) → new_esEs12(yu300, yu40000, ef, eg)
new_esEs21(yu302, yu40002, app(app(ty_@2, bbg), bbh)) → new_esEs12(yu302, yu40002, bbg, bbh)
new_esEs20(yu301, yu40001, app(ty_Ratio, bbb)) → new_esEs18(yu301, yu40001, bbb)
new_esEs6(Just(yu300), Just(yu40000), app(app(app(ty_@3, gc), gd), ge)) → new_esEs13(yu300, yu40000, gc, gd, ge)
new_esEs6(Just(yu300), Just(yu40000), app(ty_[], fh)) → new_esEs5(yu300, yu40000, fh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(app(app(ty_@3, eh), fa), fb)) → new_esEs13(yu300, yu40000, eh, fa, fb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, app(ty_[], bh)) → new_esEs5(yu310, yu40010, bh)
new_esEs20(yu301, yu40001, app(app(ty_Either, bab), bac)) → new_esEs9(yu301, yu40001, bab, bac)
new_esEs9(Left(yu300), Left(yu40000), app(ty_[], dc), bg) → new_esEs5(yu300, yu40000, dc)
new_esEs19(yu300, yu40000, ty_Float) → new_esEs17(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(ty_@2, bec), bed)) → new_esEs12(yu301, yu40001, bec, bed)
new_esEs11(GT, GT) → True
new_sr(Neg(yu3010), Neg(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_esEs20(yu301, yu40001, app(ty_Maybe, baa)) → new_esEs6(yu301, yu40001, baa)
new_esEs6(Just(yu300), Just(yu40000), ty_Integer) → new_esEs15(yu300, yu40000)
new_sr(Pos(yu3010), Pos(yu400010)) → Pos(new_primMulNat0(yu3010, yu400010))
new_asAs(False, yu33) → False
new_esEs19(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs24(yu301, yu40001, ty_Int) → new_esEs16(yu301, yu40001)
new_primEqNat0(Zero, Zero) → True
new_esEs19(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Maybe, eb)) → new_esEs6(yu300, yu40000, eb)
new_primMulNat0(Zero, Succ(yu4000100)) → Zero
new_primMulNat0(Succ(yu30100), Zero) → Zero
new_esEs19(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(ty_Maybe, fd)) → new_esEs6(yu300, yu40000, fd)
new_esEs4(yu30, yu4000, ty_Bool) → new_esEs10(yu30, yu4000)
new_esEs21(yu302, yu40002, ty_Int) → new_esEs16(yu302, yu40002)
new_esEs19(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs23(yu300, yu40000, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs13(yu300, yu40000, bdc, bdd, bde)
new_esEs22(yu310, yu40010, app(app(app(ty_@3, cc), cd), ce)) → new_esEs13(yu310, yu40010, cc, cd, ce)
new_esEs4(yu30, yu4000, ty_Int) → new_esEs16(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_Either, da), db), bg) → new_esEs9(yu300, yu40000, da, db)
new_esEs23(yu300, yu40000, app(ty_Maybe, bce)) → new_esEs6(yu300, yu40000, bce)
new_esEs19(yu300, yu40000, ty_Ordering) → new_esEs11(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs21(yu302, yu40002, ty_@0) → new_esEs7(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_[], beb)) → new_esEs5(yu301, yu40001, beb)
new_esEs22(yu310, yu40010, ty_@0) → new_esEs7(yu310, yu40010)
new_primPlusNat0(Succ(yu340), yu4000100) → Succ(Succ(new_primPlusNat1(yu340, yu4000100)))
new_esEs23(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs20(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs23(yu300, yu40000, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs23(yu300, yu40000, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_Either, ff), fg)) → new_esEs9(yu300, yu40000, ff, fg)
new_esEs19(yu300, yu40000, app(app(app(ty_@3, he), hf), hg)) → new_esEs13(yu300, yu40000, he, hf, hg)
new_esEs14(Char(yu300), Char(yu40000)) → new_primEqNat0(yu300, yu40000)
new_esEs19(yu300, yu40000, app(app(ty_Either, gh), ha)) → new_esEs9(yu300, yu40000, gh, ha)
new_esEs22(yu310, yu40010, ty_Char) → new_esEs14(yu310, yu40010)
new_primEqInt(Neg(Succ(yu3000)), Neg(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs24(yu301, yu40001, ty_Double) → new_esEs8(yu301, yu40001)
new_esEs20(yu301, yu40001, ty_Float) → new_esEs17(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Double) → new_esEs8(yu30, yu4000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Int) → new_esEs16(yu300, yu40000)
new_esEs9(Left(yu300), Left(yu40000), ty_Float, bg) → new_esEs17(yu300, yu40000)
new_primPlusNat1(Succ(yu3400), Zero) → Succ(yu3400)
new_primPlusNat1(Zero, Succ(yu40001000)) → Succ(yu40001000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Char) → new_esEs14(yu300, yu40000)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Bool) → new_esEs10(yu300, yu40000)
new_esEs16(yu30, yu4000) → new_primEqInt(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Double, bg) → new_esEs8(yu300, yu40000)
new_esEs4(yu30, yu4000, app(app(ty_@2, ca), cb)) → new_esEs12(yu30, yu4000, ca, cb)
new_esEs4(yu30, yu4000, app(app(ty_Either, bf), bg)) → new_esEs9(yu30, yu4000, bf, bg)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(yu301, yu40001, ty_Bool) → new_esEs10(yu301, yu40001)
new_esEs4(yu30, yu4000, ty_Integer) → new_esEs15(yu30, yu4000)
new_esEs9(Left(yu300), Left(yu40000), ty_Integer, bg) → new_esEs15(yu300, yu40000)
new_esEs24(yu301, yu40001, app(app(app(ty_@3, bee), bef), beg)) → new_esEs13(yu301, yu40001, bee, bef, beg)
new_esEs21(yu302, yu40002, ty_Double) → new_esEs8(yu302, yu40002)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_Integer) → new_esEs15(yu300, yu40000)
new_primEqInt(Neg(Succ(yu3000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(yu400000))) → False
new_esEs9(Left(yu300), Left(yu40000), ty_Int, bg) → new_esEs16(yu300, yu40000)
new_esEs20(yu301, yu40001, app(app(app(ty_@3, bag), bah), bba)) → new_esEs13(yu301, yu40001, bag, bah, bba)
new_esEs17(Float(yu300, yu301), Float(yu40000, yu40001)) → new_esEs16(new_sr(yu300, yu40000), new_sr(yu301, yu40001))
new_esEs19(yu300, yu40000, ty_Double) → new_esEs8(yu300, yu40000)
new_esEs22(yu310, yu40010, ty_Integer) → new_esEs15(yu310, yu40010)
new_esEs10(False, False) → True
new_esEs21(yu302, yu40002, ty_Float) → new_esEs17(yu302, yu40002)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs19(yu300, yu40000, ty_Integer) → new_esEs15(yu300, yu40000)
new_esEs22(yu310, yu40010, app(app(ty_@2, ca), cb)) → new_esEs12(yu310, yu40010, ca, cb)
new_asAs(True, yu33) → yu33
new_primMulNat0(Succ(yu30100), Succ(yu4000100)) → new_primPlusNat0(new_primMulNat0(yu30100, Succ(yu4000100)), yu4000100)
new_esEs6(Just(yu300), Just(yu40000), ty_Float) → new_esEs17(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), ty_Double) → new_esEs8(yu300, yu40000)
new_esEs11(LT, LT) → True
new_esEs4(yu30, yu4000, ty_@0) → new_esEs7(yu30, yu4000)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs24(yu301, yu40001, ty_@0) → new_esEs7(yu301, yu40001)
new_esEs22(yu310, yu40010, ty_Double) → new_esEs8(yu310, yu40010)
new_esEs6(Nothing, Nothing, be) → True
new_esEs21(yu302, yu40002, ty_Char) → new_esEs14(yu302, yu40002)
new_primEqInt(Pos(Succ(yu3000)), Pos(Succ(yu400000))) → new_primEqNat0(yu3000, yu400000)
new_esEs9(Left(yu300), Left(yu40000), app(app(app(ty_@3, df), dg), dh), bg) → new_esEs13(yu300, yu40000, df, dg, dh)
new_esEs21(yu302, yu40002, app(ty_Maybe, bbc)) → new_esEs6(yu302, yu40002, bbc)
new_esEs6(Just(yu300), Just(yu40000), ty_Int) → new_esEs16(yu300, yu40000)
new_esEs6(Just(yu300), Just(yu40000), app(app(ty_@2, ga), gb)) → new_esEs12(yu300, yu40000, ga, gb)
new_esEs9(Right(yu300), Right(yu40000), bf, ty_@0) → new_esEs7(yu300, yu40000)
new_esEs26(yu301, yu40001, ty_Integer) → new_esEs15(yu301, yu40001)
new_esEs24(yu301, yu40001, ty_Char) → new_esEs14(yu301, yu40001)
new_esEs6(Nothing, Just(yu40000), be) → False
new_esEs6(Just(yu300), Nothing, be) → False
new_primEqNat0(Succ(yu3000), Succ(yu400000)) → new_primEqNat0(yu3000, yu400000)
new_esEs11(GT, EQ) → False
new_esEs11(EQ, GT) → False
new_esEs24(yu301, yu40001, app(ty_Maybe, bdg)) → new_esEs6(yu301, yu40001, bdg)
new_esEs9(Left(yu300), Left(yu40000), app(ty_Ratio, ea), bg) → new_esEs18(yu300, yu40000, ea)
new_esEs21(yu302, yu40002, ty_Bool) → new_esEs10(yu302, yu40002)
new_esEs24(yu301, yu40001, app(ty_Ratio, beh)) → new_esEs18(yu301, yu40001, beh)
new_esEs9(Right(yu300), Right(yu40000), bf, app(ty_Ratio, fc)) → new_esEs18(yu300, yu40000, fc)
new_esEs7(@0, @0) → True
new_esEs21(yu302, yu40002, app(app(ty_Either, bbd), bbe)) → new_esEs9(yu302, yu40002, bbd, bbe)
new_esEs12(@2(yu300, yu301), @2(yu40000, yu40001), ca, cb) → new_asAs(new_esEs23(yu300, yu40000, ca), new_esEs24(yu301, yu40001, cb))
new_esEs9(Left(yu300), Left(yu40000), app(app(ty_@2, dd), de), bg) → new_esEs12(yu300, yu40000, dd, de)
new_esEs4(yu30, yu4000, ty_Char) → new_esEs14(yu30, yu4000)
new_esEs19(yu300, yu40000, app(ty_[], hb)) → new_esEs5(yu300, yu40000, hb)
new_esEs24(yu301, yu40001, app(app(ty_Either, bdh), bea)) → new_esEs9(yu301, yu40001, bdh, bea)
new_primEqInt(Pos(Succ(yu3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu400000))) → False
new_esEs22(yu310, yu40010, ty_Ordering) → new_esEs11(yu310, yu40010)
new_esEs9(Right(yu300), Left(yu40000), bf, bg) → False
new_esEs9(Left(yu300), Right(yu40000), bf, bg) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs21(yu302, yu40002, app(ty_Ratio, bcd)) → new_esEs18(yu302, yu40002, bcd)
new_esEs22(yu310, yu40010, ty_Int) → new_esEs16(yu310, yu40010)
new_esEs5(:(yu310, yu311), :(yu40010, yu40011), bd) → new_asAs(new_esEs22(yu310, yu40010, bd), new_esEs5(yu311, yu40011, bd))
new_esEs6(Just(yu300), Just(yu40000), app(ty_Ratio, gf)) → new_esEs18(yu300, yu40000, gf)
The set Q consists of the following terms:
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs23(x0, x1, ty_Int)
new_esEs6(Just(x0), Nothing, x1)
new_esEs21(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs9(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs7(@0, @0)
new_esEs6(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Char)
new_esEs6(Nothing, Nothing, x0)
new_esEs25(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5([], [], x0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs9(Left(x0), Left(x1), ty_Integer, x2)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs9(Left(x0), Left(x1), ty_Int, x2)
new_esEs6(Just(x0), Just(x1), ty_Double)
new_asAs(True, x0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs6(Just(x0), Just(x1), ty_@0)
new_esEs9(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Left(x0), Left(x1), ty_Char, x2)
new_esEs5([], :(x0, x1), x2)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_esEs12(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs6(Nothing, Just(x0), x1)
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Integer)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs9(Right(x0), Right(x1), x2, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Zero, x0)
new_esEs24(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Integer)
new_esEs9(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs19(x0, x1, ty_Double)
new_esEs6(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Ordering)
new_esEs9(Left(x0), Left(x1), ty_@0, x2)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Just(x0), Just(x1), ty_Bool)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs9(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs21(x0, x1, ty_Int)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs9(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_esEs4(x0, x1, ty_Float)
new_esEs9(Right(x0), Left(x1), x2, x3)
new_esEs9(Left(x0), Right(x1), x2, x3)
new_esEs19(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Integer)
new_esEs10(False, False)
new_esEs24(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Double)
new_esEs15(Integer(x0), Integer(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs6(Just(x0), Just(x1), ty_Int)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Zero)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs9(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs9(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, ty_Double)
new_esEs11(GT, GT)
new_esEs9(Right(x0), Right(x1), x2, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Char)
new_esEs6(Just(x0), Just(x1), app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_sr(Pos(x0), Pos(x1))
new_esEs9(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs14(Char(x0), Char(x1))
new_esEs9(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs9(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs9(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs6(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Float)
new_esEs9(Right(x0), Right(x1), x2, ty_Int)
new_esEs26(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs11(LT, LT)
new_esEs21(x0, x1, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, ty_Char)
new_esEs9(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Bool)
new_esEs9(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Float)
new_primPlusNat1(Zero, Zero)
new_esEs9(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Int)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs10(True, True)
new_esEs16(x0, x1)
new_esEs5(:(x0, x1), [], x2)
new_esEs22(x0, x1, ty_Bool)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(EQ, EQ)
new_esEs6(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Integer)
new_esEs6(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Int)
new_esEs22(x0, x1, ty_Ordering)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs24(x0, x1, app(ty_Maybe, x2))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_lookup1(yu13, yu14, yu15, yu16, yu17, yu18, False, ba, bb) → new_lookup(:(yu13, yu14), yu18, ba, bb)
The graph contains the following edges 6 >= 2, 8 >= 3, 9 >= 4
- new_lookup(:(yu30, yu31), :(@2([], yu401), yu41), bc, bd) → new_lookup(:(yu30, yu31), yu41, bc, bd)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4
- new_lookup(:(yu30, yu31), :(@2(:(yu4000, yu4001), yu401), yu41), bc, bd) → new_lookup1(yu30, yu31, yu4000, yu4001, yu401, yu41, new_asAs(new_esEs4(yu30, yu4000, bd), new_esEs5(yu31, yu4001, bd)), bc, bd)
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3, 2 > 4, 2 > 5, 2 > 6, 3 >= 8, 4 >= 9